\begin{tabbing}
p{-}inject($A$;$B$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$, $y$:$A$.\+
\\[0ex]($\uparrow$can{-}apply($f$;$x$)) $\Rightarrow$ ($\uparrow$can{-}apply($f$;$y$)) $\Rightarrow$ (do{-}apply($f$;$x$) = do{-}apply($f$;$y$)) $\Rightarrow$ ($x$ = $y$)
\-
\end{tabbing}